(declare-const x Float32)
(declare-const y Float32)
(declare-const z Float32)
(declare-const r Float32)
(assert (= x (fp #b0 #b01111111 #b11011101101101101000101)))
(assert (= y (fp #b0 #b01111111 #b11101100000111000100001)))
(assert (= z (fp #b0 #b01100111 #b10100111110110000110101)))
(assert (= r (fp #b0 #b10000000 #b11001011001001111100011)))
(assert (not (= (fp.fma RNE x y z) r)))
(check-sat)
